strongwellfounded($T$; $x$,$y$.$R$($x$;$y$)) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$f$:$T$$\rightarrow\mathbb{N}$. ($\forall$$x$:$T$, $y$:$T$. $R$($x$;$y$) $\Rightarrow$ (($f$($x$)) $<$ ($f$($y$))))